Nuprl Lemma : decidable_decision
4,23
postcript
pdf
P
:Prop,
x
:Dec(
P
).
x
Decision
latex
Definitions
Dec(
P
)
,
Decision
,
P
Q
,
False
,
P
Q
,
S
T
,
Top
,
Prop
,
t
T
,
A
,
x
:
A
.
B
(
x
)
Lemmas
not
wf
,
top
wf
origin
P:Prop, x:Dec(P). x 
Decision P:Prop, x:Dec(P). x Decision 
Q
Q
T T
Ax:A. B(x)